Nuprl Lemma : component_wf
11,40
postcript
pdf
ds
:(Id
Type{i}),
da
:(Id
Knd
Type{i}),
A
,
B
:Type{i}.
component{i:l}(
ds
;
da
;
A
;
B
)
Type{i'}
latex
Definitions
Type
,
t
T
,
Id
,
x
:
A
B
(
x
)
,
Knd
,
x
:
A
.
B
(
x
)
,
Interface(
ds
;
da
;
A
)
,
RealizerScheme{i:l}()
,
x
:
A
B
(
x
)
,
Component(
ds
;
da
;
A
;
B
)
Lemmas
RealizerScheme
wf
,
interface
wf
,
Knd
wf
,
Id
wf
origin
ds:(Id
Type{i}), da:(IdKndType{i}), A, B:Type{i}.
Type{i'} ds:(IdType{i}), da:(IdKndType{i}), A, B:Type{i}.
Type{i'} TB(x)x:A. B(x)
B(x)